k:Knd, l:IdLnk, ds:x:Id fp Type, da:a:Knd fp Type,
f:(tg:Id(State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List.
with declarations ds:dsda:dak(v) sends f s v on link l  MsgA 

latex

Definitions	with declarations ds:dsda:dak(v) sends f s v on link l, mk-ma, locl(a), Prop, IdDeq, x : v, 1of(t), 2of(t), , State(ds), Valtype(da;k), f(x)?z, KindDeq, rcv(l,tg), a:A fp B(a), x:A. B(x), x. t(x), Id, IdLnk, t  T, Knd
Lemmas	Knd wf, IdLnk wf, Id wf, fpf wf, rcv wf, Kind-deq wf, fpf-cap wf, ma-valtype wf, ma-state wf, fpf-empty wf, pi2 wf, pi1 wf, fpf-single wf, id-deq wf, locl wf, mk-ma wf